Nuprl Lemma : es-E-interface-subtype
11,40
postcript
pdf
es
:ES,
X
:AbsInterface(Top). E(
X
)
E
latex
Definitions
E(
X
)
,
S
T
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
E
,
Type
,
b
,
e
X
,
AbsInterface(
A
)
,
x
:
A
.
B
(
x
)
,
Top
,
t
T
,
ES
Lemmas
event
system
wf
,
top
wf
,
es-interface
wf
,
es-is-interface
wf
,
assert
wf
,
es-E
wf
origin
es:ES, X:AbsInterface(Top). E(X) 
E es:ES, X:AbsInterface(Top). E(X) E T
B(x)
b
Xx:A. B(x) T